T, I:Type, P:(I(T List)Prop). (x:I. safety(T;L.P(x,L)))  safety(T;L.x:I. P(x,L)) 

latex

Definitions	t  T, x:A. B(x), l1  l2, x(s1,s2), Prop, P  Q, safety(A;tr.P(tr)), x. t(x)
Lemmas	safety wf, iseg wf